package at.ttasat;

import java.io.ByteArrayOutputStream;
import java.io.File;
import java.io.FileInputStream;

import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintStream;
import java.util.Random;

import at.ltasat.solve.SolverConfiguration;
import at.ltasat.solve.SolverMain;
import at.tasat.Configuration;
import at.tasat.Main;

public class SolverSpeedtest {
	private final TasatType tasatType;
	private final String[] parameters;
	private final int runs;
	private final long startSeed;
	private final RunResult[] results;
	private final int maximalVariables;
	private final int maximalClauses;
	private final double weightingFactor;

	public SolverSpeedtest(TasatType tasatType, String[] parameters, SolverTestResult result) {
		this(tasatType, parameters, result.getRuns(), result.getStartSeed(), result.getMaximalVariables(), result.getMaximalClauses(), result.getWeightingFactor());
	}

	public SolverSpeedtest(TasatType tasatType, String[] parameters, int runs, long startSeed, int maximalVariables, int maximalClauses, double weightingFactor) {
		this.tasatType = tasatType;
		this.parameters = parameters;
		this.runs = runs;
		this.startSeed = startSeed;
		this.maximalVariables = maximalVariables;
		this.maximalClauses = maximalClauses;
		this.weightingFactor = weightingFactor;
		results = new RunResult[runs];
	}

	public SolverTestResult test() throws IOException {
		System.out.println("Starting test");
		System.out.println("Runs: " + runs);
		System.out.println("Seed: " + startSeed);
		System.out.println("Maximal Variables: " + maximalVariables);
		System.out.println("Maximal Clauses: " + maximalClauses);
		System.out.println("Weighting Factor: " + weightingFactor);
		System.out.println();
		System.out.print("Warmup ");
		runTest(startSeed); // warm up
		Random random = new Random(startSeed);
		for (int i = 0; i < runs; i++) {
			results[i] = runTest(random.nextLong());
		}
		System.out.println();
		System.out.println("Test finished");
		return new SolverTestResult(tasatType, parameters, runs, startSeed, results, maximalVariables, maximalClauses, weightingFactor);
	}

	private RunResult runTest(long seed) throws IOException {
		try {
			RunDescription runDescription = new RunDescription(seed, maximalVariables, maximalClauses, weightingFactor);
			System.out.println("Run Seed=" + seed + " Variables=" + runDescription.getVariables() + " Clauses=" + runDescription.getClauses());
			File cnfFile = getCnf(runDescription);
			ByteArrayOutputStream out = new ByteArrayOutputStream();
			PrintStream outPrintStream = new PrintStream(out);

			ByteArrayOutputStream error = new ByteArrayOutputStream();
			PrintStream errorPrintStream = new PrintStream(error);

			long startTime = System.currentTimeMillis();
			switch (tasatType) {
			case Tasat: {
				FileInputStream fileStream = new FileInputStream(cnfFile);
				Configuration config = Configuration.get(parameters);
				config.setIn(fileStream);
				config.setOut(outPrintStream);
				config.setErr(errorPrintStream);
				Main.main(config);
				fileStream.close();
			}
				break;
			case P_Tasat: {
				at.ptasat.Configuration config = at.ptasat.Configuration.get(parameters);
				config.setIn(cnfFile);
				config.setOut(outPrintStream);
				config.setErr(errorPrintStream);
				at.ptasat.Main.main(config);
			}
				break;
			case L_Tasat: {
				SolverConfiguration config = SolverConfiguration.get(parameters);
				config.setIn(cnfFile);
				config.setOut(outPrintStream);
				config.setErr(errorPrintStream);
				SolverMain.main(config);
			}
				break;
			}
			long time = System.currentTimeMillis() - startTime;
			outPrintStream.close();
			errorPrintStream.close();
			String errors = error.toString();
			if (errors.length() > 0) {
				throw new Exception(errors);
			}
			cnfFile.delete();
			String resultString = out.toString();
			return new RunResult(time, resultString.contains("s SATISFIABLE"));
		} catch (Throwable t) {
			System.out.println("\n**************************************************************");
			System.out.println(" Solver failed; Seed=" + seed);
			System.out.print(t.toString());
			System.out.println("\n**************************************************************");
			throw new RuntimeException(t);
		}
	}

	private File getCnf(RunDescription runDescription) throws IOException {
		String dimacsString = runDescription.getDimacsString();
		File cnfFile = File.createTempFile("testCnf" + runDescription, ".dimacs");
		FileWriter writer = new FileWriter(cnfFile);
		writer.write(dimacsString);
		writer.close();
		return cnfFile;
	}
}
